E, A:Type, info:(E(IdA+(IdLnkE)Id)), e:E. rcv?(e)  rtag(info;e)  Id 

latex

Definitions	rcv?(e), rtag(info;e), ecase1(e;info;i.f(i);l,e'.g(l;e')), x:A. B(x), Id, IdLnk, b, False, P  Q, t  T, True
Lemmas	true wf, false wf, IdLnk wf, Id wf, rcv? wf, assert wf